Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y
Q is empty.
↳ QTRS
↳ DirectTerminationProof
Q restricted rewrite system:
The TRS R consists of the following rules:
\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y
Q is empty.
We use [23] with the following order to prove termination.
Lexicographic path order with status [19].
Quasi-Precedence:
/2 > [\2, e]
.2 > [\2, e]
Status: e: multiset
\2: [2,1]
.2: multiset
/2: [2,1]